ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), a:ecl(ds; da), es:event_system{i:l}, i:Id.
(x:Id. subtype_rel(es-vartype(es; i; x); fpf-cap(ds; id-deq; x; top)))
 (e:es-E(es). (loc(e) = i)  subtype_rel(es-valtype(es; e); ma-valtype(da; es-kind(es; e))))
 (n:, e1,e2:{e:es-E(es)| loc(e) = i} .
 (es-bact{i:l}(ds; da; a; es; n; e1; e2))  (ecl-es-act(es; n; a)(e1,e2))) 

latex

Definitions	P  Q, P  Q, True, if b then t else f fi , ff, tt, b, P  Q, , ecl(ds; da), fpf(A; a.B(a)), es-bact{i:l}(ds; da; a; es; n; e1; e2), prop{i:l}, x. t(x), t  T, P  Q, x:A. B(x), False, A, P  Q, decidable(P), x(s)
Lemmas	false wf, true wf, le wf, bool wf, decl-state wf, l member wf, decidable wf, Knd wf, fpf wf, ecl wf, event system wf, top wf, id-deq wf, fpf-cap wf, es-vartype wf, es-kind wf, ma-valtype wf, es-valtype wf, nat wf, es-loc wf, Id wf, es-E wf, ecl-es-act wf